CHOICE-STRATEGY-IS: 
@(UNIT C1)∨@(UNIT C2);

EDIT-STRATEGY-IS: 
α(C)>3∨∂(C)>4;


PARMODULATE =T
EQUAL-SYMBOL =NIL
PAR-DEPTH-BOUND =101
ELAPSED-TIME =129032

NIL 1 2
1 ¬f((SB(A)∩ SB(B)),SB((A ∩ B)))⊂(A ∩ B);3 4
2 x ⊂ y∧x ⊂ z⊃x ⊂(y ∩ z);a5
3 ¬f((SB(A)∩ SB(B)),SB((A ∩ B)))ε SB((A ∩ B));5 6
4 x ⊂ y∧x ε U⊃x ε SB(y);a7
5 ¬(SB(A)∩ SB(B))≡ SB((A ∩ B));THEOREM
6 f(x,y)ε x∧f(x,y)ε y⊃x ≡ y;a1